This is TeX, WAITS Version 1.1 (preloaded format=cplain 84.8.28)  11 SEP 1984 16:08
**provin
(PROVIN.TEX[B2,JMC] (CLTEX.FIX[TEX,CLT]) (BMAC.TEX[B2,JMC]) (BMAC.FIX[B2,JMC]
\sxfam=\fam11
)
\unit=\dimen18

(PROVA.[B2,JMC] Chapter 1. [1] [2] [3] [4]
Overfull \hbox (12.89552pt too wide) in paragraph at lines 99--101, p.3
[]\tenrm 2. If $↑↑I$ is an n-ary func-tion ex-pres-sion and $\teni t[]; t[] [] t
[]$ \tenrm are terms then $↑↑I[\teni t[]; t[]; [] t[]\tenrm ]$|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\hbox(0.0+0.0)x20.0
.\tenrm 2
.\tenrm .
.\glue 4.44443 plus 4.99997 minus 0.37036
.\tenrm I
.etc.

[5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20]
[21] [22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34])
(PROVB.[B2,JMC] [35] [36] [37] [38] [39] [40]
Overfull \hbox (14.42632pt too wide) in paragraph at lines 235--238, p.2
\tenrm ing $[]$. No-tice that the pre-vi-ous ex-er-cises im-ply that we ac-tu-al
ly have $\tensy 8\teni X  [] \tenrm [\teni X\tenrm ] =|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\tenrm i
.\tenrm n
.\tenrm g
.\glue 3.33333 plus 1.66666 minus 1.1111
.\mathon
.etc.

[41] [42] [43] [44] [45]
Overfull \hbox (12.11229pt too wide) in paragraph at lines 13--16, p.6
\tenbf Base case: \tenrm Sup-pose that $\teni x$ \tenrm is an atom and $\teni y$
\tenrm ,$\teni ↑↑K \tensy 2 A \tenit l[]$ \tenrm are such that $[] [\teni x;  y;
  ↑↑K\tenrm ] \tensy 6\tenrm =|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\tenbf B
.\tenbf a
.\tenbf s
.\tenbf e
.\glue 3.83333 plus 1.91666 minus 1.27777
.etc.


Overfull \hbox (6.50246pt too wide) in paragraph at lines 34--37, p.6
[]\tenrm In the sec-ond case, since $[] [\teni x;  y;  ↑↑K\tenrm ] \tensy 6\tenr
m = []$, we must have that $[] [\teni x;  y;  ↑↑K\tenrm ] =|

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\hbox(0.0+0.0)x20.0
.\tenrm I
.\tenrm n
.\glue 3.33333 plus 1.66666 minus 1.1111
.\tenrm t
.etc.

[46] [47] [48] [49] [50] [51]
Overfull \hbox (17.74931pt too wide) in paragraph at lines 49--49, p.10
[]|\ninett (defun subsub (a b) (if (null a) a (cons (cons (caar a) (sublis (cdar
 a) b)) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\ninett (
.\ninett d
.\ninett e
.etc.

[52]
Overfull \hbox (8.29933pt too wide) in paragraph at lines 19--19, p.11
[]|        \ninett ((isvar x) (if (occur x y) 'no (compose a (cons (cons x y) ni
l)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.


Overfull \hbox (8.29933pt too wide) in paragraph at lines 20--20, p.11
[]|        \ninett ((isvar y) (if (occur y x) 'no (compose a (cons (cons y x) ni
l)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.

[53] [54] [55] [56] [57] [58] [59] [60] [61] [62]
Overfull \hbox (27.1993pt too wide) in paragraph at lines 14--14, p.17
[]|        \ninett ((isvar x) (if (v-occur x y a) 'no (compose a (cons (cons x y
) nil)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.


Overfull \hbox (27.1993pt too wide) in paragraph at lines 15--15, p.17
[]|        \ninett ((isvar y) (if (v-occur y x a) 'no (compose a (cons (cons y x
) nil)))) |

\hbox(8.0+3.0)x361.34999
.\hbox(0.0+0.0)x20.0
.\rule(8.0+3.0)x0.0
.\glue 4.72499
.\glue 4.72499
.\glue 4.72499
.etc.

) [63]
Output written on PROVIN.DVI[B2,JMC] (63 pages, 185544 bytes).